(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 18) (_ BitVec 22)) (_ BitVec 65))
(declare-fun p0 ( (_ BitVec 29)) Bool)
(declare-fun v0 () (_ BitVec 84))
(declare-fun v1 () (_ BitVec 65))
(declare-fun v2 () (_ BitVec 59))
(assert (let ((e3(_ bv18468138584850704555417399425240 104)))
(let ((e4 (bvor v1 ((_ sign_extend 6) v2))))
(let ((e5 (f0 ((_ extract 22 5) v1) ((_ extract 41 20) e3))))
(let ((e6 (ite (p0 ((_ extract 47 19) e3)) (_ bv1 1) (_ bv0 1))))
(let ((e7 (bvnand e4 e5)))
(let ((e8 (bvsrem ((_ sign_extend 39) e7) e3)))
(let ((e9 (bvadd ((_ sign_extend 39) e4) e3)))
(let ((e10 (bvadd e4 e5)))
(let ((e11 (bvor e7 v1)))
(let ((e12 (bvxor e3 ((_ sign_extend 103) e6))))
(let ((e13 (bvmul ((_ zero_extend 19) e5) v0)))
(let ((e14 (bvslt e8 ((_ zero_extend 39) e10))))
(let ((e15 (bvugt e5 e7)))
(let ((e16 (p0 ((_ extract 55 27) e8))))
(let ((e17 (bvsge ((_ sign_extend 20) e13) e12)))
(let ((e18 (bvsgt ((_ sign_extend 20) e13) e9)))
(let ((e19 (bvsgt e9 ((_ zero_extend 39) v1))))
(let ((e20 (bvslt ((_ zero_extend 39) e10) e8)))
(let ((e21 (distinct ((_ sign_extend 25) v2) v0)))
(let ((e22 (= e8 ((_ zero_extend 45) v2))))
(let ((e23 (bvuge v1 e11)))
(let ((e24 (bvsgt e9 ((_ zero_extend 39) e11))))
(let ((e25 (= ((_ zero_extend 64) e6) v1)))
(let ((e26 (bvsgt e9 e9)))
(let ((e27 (bvsle e7 e10)))
(let ((e28 (bvsle ((_ sign_extend 58) e6) v2)))
(let ((e29 (bvsge e5 v1)))
(let ((e30 (bvsge ((_ sign_extend 39) v1) e9)))
(let ((e31 (bvule e12 ((_ sign_extend 20) e13))))
(let ((e32 (bvugt e8 e3)))
(let ((e33 (bvsgt e12 ((_ zero_extend 39) e5))))
(let ((e34 (bvule ((_ zero_extend 19) e4) e13)))
(let ((e35 (= e22 e22)))
(let ((e36 (ite e25 e20 e15)))
(let ((e37 (ite e26 e27 e31)))
(let ((e38 (or e24 e24)))
(let ((e39 (= e16 e36)))
(let ((e40 (and e23 e18)))
(let ((e41 (and e21 e37)))
(let ((e42 (ite e14 e28 e14)))
(let ((e43 (not e34)))
(let ((e44 (= e43 e30)))
(let ((e45 (and e39 e42)))
(let ((e46 (not e32)))
(let ((e47 (xor e38 e33)))
(let ((e48 (or e44 e41)))
(let ((e49 (or e47 e19)))
(let ((e50 (=> e45 e48)))
(let ((e51 (or e49 e29)))
(let ((e52 (not e17)))
(let ((e53 (not e46)))
(let ((e54 (not e53)))
(let ((e55 (ite e35 e50 e52)))
(let ((e56 (not e40)))
(let ((e57 (and e51 e56)))
(let ((e58 (and e54 e55)))
(let ((e59 (= e57 e58)))
(let ((e60 (and e59 (not (= e3 (_ bv0 104))))))
(let ((e61 (and e60 (not (= e3 (bvnot (_ bv0 104)))))))
e61
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
